;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "MColorThreshold.lisp")
(require "Mimage.lisp")
(require "MCommon.lisp")

(module TColorThreshold
  (include-book "list-utilities" :dir :teachpacks)
  (include-book "io-utilities" :dir :teachpacks)
  (include-book "avl-rational-keys" :dir :teachpacks)
  (include-book "doublecheck" :dir :teachpacks)
  (include-book "testing" :dir :teachpacks)
  
  (import ICommon)
  (import IImage)
  (import IColorThreshold)

  (defconst *header* (list 1 2 3 4 5 6))
  (defconst *width* 2)
  (defconst *height* 2)
  (defconst *tree1* (avl-insert (avl-insert (avl-insert (empty-tree) -1 *header*) -2 *width*) -3 *height*))
  (defconst *tree2* (insertPixel *tree1* 1 2 100 100 100))
  (defconst *tree3* (insertPixel *tree2* 2 2 105 105 105))
  (defconst *tree4* (insertPixel *tree3* 1 1 110 110 110))
  (defconst *tree5* (insertPixel *tree4* 2 1 115 115 115))

   ; Generates a random pixel (random RGB values).
  (defrandom random-pixel ()
    (let* ((r (random-between 0 255))
           (g (random-between 0 255))
           (b (random-between 0 255)))
      (list r g b)))

  ; creates a bitmap tree of random pixels
  (defun fill-bitmap (tr width height x y pixels)
    (if (and (posp y) (<= y height))
        (if (and (posp x) (<= x width))
            (fill-bitmap (insertPixel tr x y (caar pixels) (cadar pixels) (caddar pixels))
                         width height (+ x 1) y (cdr pixels))
            (fill-bitmap tr width height 1 (+ y 1) pixels))
        tr))
            
  ; creates a bitmap tree of random pixels for testing in property definitions
  (defrandom random-bitmap (width height)
    (fill-bitmap 
     (avl-insert (avl-insert (avl-insert (empty-tree) -1 *header*) -2 width) -3 height)
     width height 1 1 (random-list-of (random-pixel) :size (* width height))))
  
  ; creates a bitmap tree in which each pixel is the same color for testing 
  ; in property definitions
  (defrandom random-monocol-bitmap (width height pixel)
    (fill-bitmap 
     (avl-insert (avl-insert (avl-insert (empty-tree) -1 *header*) -2 width) -3 height)
     width height 1 1 (random-list-of pixel :size (* width height))))

  ; Check-Expects
  ; pixelLessThanColorThreshold
  (check-expect (pixelLessThanColorThreshold (createRGB 150 50 100)
                                             (createRGB 200 100 150)) t)
  (check-expect (pixelLessThanColorThreshold (createRGB 200 100 100) 
                                             (createRGB 200 100 100)) t)
  (check-expect (pixelLessThanColorThreshold (createRGB 220 130 150)
                                             (createRGB 200 100 100)) nil)

  ; processColorThreshold
  (check-expect (equal (getPixel 
                        (processColorThreshold *tree5* (createRGB 108 108 108)
                                               (createRGB 144 144 144) 1
                                               *height* *width* *height*) 2 2)
                       (createRGB 144 144 144)) t)
  (check-expect (equal (getPixel 
                        (processColorThreshold *tree5* (createRGB 108 108 108)
                                               (createRGB 144 144 144) 1
                                               *height* *width* *height*) 1 1)
                       (createRGB 144 144 144)) nil)
  
  ; MainColorThreshold
  (check-expect (getPixel (car (MainColorThreshold *tree5* (list 105 105 105 130 160 190))) 1 2)
                (createRGB 130 160 190))
  (check-expect (getPixel (car (MainColorThreshold *tree5* (list 105 105 105 130 160 190))) 1 1)
                (createRGB 110 110 110))

  ; Property definitions
  ; processColorThreshold
  ; Verifies that processColorThreshold always returns a non-empty avl-tree
  ; with RGB color lists at each node
  (defproperty process-color-threshold-returns-proper-bitmap-tree-prp
    (width :value (random-between 1 15)
     height :value (random-between 1 15)
     thresholdValue :value (random-list-of (random-between 0 255) :size 3)
     newColor :value (random-list-of (random-between 0 255) :size 3)
     bitmap :value (random-bitmap width height))
    (let* ((newBmp (processColorThreshold bitmap thresholdValue newColor 
                                          1 height width height))
           (pixel (getPixel newBmp width height))) 
      (and (tree? newBmp) (not (empty-tree? newBmp))
           (consp pixel) (= (len pixel) 3) (natp (car pixel)) 
           (< (car pixel) 256) (natp (cadr pixel)) (< (cadr pixel) 256)
           (natp (caddr pixel)) (< (caddr pixel) 256))))
  
  ; Verifies that processColorThreshold changes the pixels at or below the
  ; threshold to the given new color
  (defproperty process-color-threshold-changes-pixels-below-threshold-prp
    (width :value (random-between 1 15)
     height :value (random-between 1 15)
     thresholdValue :value (random-list-of (random-between 0 255) :size 3)
     newColor :value (random-list-of (random-between 0 255) :size 3)
     x :value (random-between 1 width)
     y :value (random-between 1 height)
     bitmap :value (random-monocol-bitmap width height 
                                          (createRGB (random-between 0 (car thresholdValue))
                                                     (random-between 0 (cadr thresholdValue))
                                                     (random-between 0 (caddr thresholdValue))))
     newBmp :value (processColorThreshold bitmap thresholdValue newColor 
                                          1 height width height))
    (equal (getPixel newBmp x y) newColor))

  ; Verifies that processColorThreshold does not change pixels above the threshhold color
  (defproperty process-color-threshold-ignores-pixels-above-threshold-prp
    (width :value (random-between 1 15)
     height :value (random-between 1 15)
     thresholdValue :value (random-list-of (random-between 0 127) :size 3)
     newColor :value (random-list-of (random-between 0 255) :size 3)
     x :value (random-between 1 width)
     y :value (random-between 1 height)
     bitmap :value (random-monocol-bitmap width height 
                                          (createRGB (random-between 
                                                      (+ (car thresholdValue) 1) 255)
                                                     (random-between 
                                                      (+ (cadr thresholdValue) 1) 255)
                                                     (random-between 
                                                      (+ (caddr thresholdValue) 1) 255)))
     newBmp :value (processColorThreshold bitmap thresholdValue newColor 
                                          1 height width height))
    (equal (getPixel newBmp x y) (getPixel bitmap x y)))
  
  ; Verifies that MainColorThreshold returns a multiple-value containing a tree
  ; and a success message given valid input
  (defproperty main-color-threshold-returns-correct-mv-prp
    (width :value (random-between 1 15)
     height :value (random-between 1 15)
     bitmap :value (random-bitmap width height)
     args :value (random-list-of (random-between 0 255) :size 6))
    (let* ((mVal (MainColorThreshold bitmap args)))
      (and (tree? (car mVal)) (not (empty-tree? (car mVal)))
           (string-equal (caadr mVal) 
                         "Successfully applied color threshold to image."))))
  )

  (link RTColorThreshold
        (MCommon MImage MColorThreshold TColorThreshold))  
  
  (invoke RTColorThreshold)